package arlab.formulae.tests
import arlab.formulae._
import arlab.formulae.transformations._

object Blatt3 {
    def main (args: Array[String]) ={
        var m = Map():Map[Variable,Term]
        m=m.updated(Variable("a"), Variable("b"))
        m=m.updated(Variable("b"), Variable("c"))
        m=m.updated(Variable("c"), Variable("d"))
        m=m.updated(Variable("x"), Variable("b"))
        m=m.updated(Variable("y"), Variable("c"))
        m=m.updated(Variable("z"), Variable("d"))

        
        val b = Function ("f",Variable("a"), Variable("b"), Variable("a")) 
        println("normal:")
        println(b)
        println("functions:")
        println(b.functions)
        println("substituiert: a->b, b->c, c->d, x->b, y->c, z->d, x->b, y->c, z->d")
        println(b.subst(m))
      
        val c = Predicate("P",Variable("x"))&&(ForAll(Variable("x"),Predicate("Q",Variable("x"))||(Predicate("R",Variable("y"))&&(Exists(Variable("y"),Predicate("P",Variable("y")))))))
        println("normal:")
        println(c)
        println("functions:")
        println(c.functions)
        println("bound-Var:")
        println(c.bound)
        println("free-Var:")
        println(c.free)
        println("substituiert: a->b, b->c, c->d, x->b, y->c, z->d")
        println(c.subst(m))
        println("skol:")
        println(Transformations.skolemize(c))
        println("pnf:")
        println(Transformations.pnf(c))

        val d = ForAll(Variable("x"),Predicate("P",Variable("x"),Variable("y")))
        println("normal:")
        println(d)
        println("functions:")
        println(d.functions)
        println("bound-Var:")
        println(d.bound)
        println("free-Var:")
        println(d.free)
        println("substituiert: a->b, b->c, c->d, x->b, y->c, z->d")
        println(d.subst(m))
        println("skol:")
        println(Transformations.skolemize(d))
        println("pnf:")
        println(Transformations.pnf(d))

        val e = Function("f",Variable("x"),Variable("y"))
        println("normal:")
        println(e)
        println("functions:")
        println(e.functions)
        println("bound-Var:")
        println(e.bound)
        println("free-Var:")
        println(e.free)
        println("substituiert: a->b, b->c, c->d, x->b, y->c, z->d")
        println(e.subst(m))
      
        val f = ForAll(Variable("y"),Exists(Variable("z"),Predicate("P",Variable("y"),Function("f",Variable("z")))||(Predicate("P",Function("f",Variable("z")),Variable("y")))&&(-(Predicate("P",Function("f",Variable("x")),Variable("z"))))))
        println("normal:")
        println(f)
        println("functions:")
        println(f.functions)
        println("bound-Var:")
        println(f.bound)
        println("free-Var:")
        println(f.free)
        println("substituiert: a->b, b->c, c->d, x->b, y->c, z->d")
        println(f.subst(m))
        println("skol:")
        println(Transformations.skolemize(f))
        println("pnf:")
        println(Transformations.pnf(f))
        
        val g = ForAll(Variable("d"), Predicate("P", Variable("d"), Variable("c")))
        println("normal:")
        println(g)
        println("substituiert: a->b, b->c, c->d, x->b, y->c, z->d")
        println(g.subst(m))
    }
}
